Revert Makefile changes from 13023:70155087efe89 -- they break make dist.

Signed-off-by: Ewan Mellor <ewan@xensource.com>

diff --git a/tools/Makefile b/tools/Makefile
index 8cc4e1cd31d8caab14be769c1801601270f267f1..b4156fc90435e496888824aa41c0f68220d939fe 100644 (file)
--- a/tools/Makefile
+++ b/tools/Makefile
@@ -36,7 +36,7 @@ all: check
        $(MAKE) ioemu
 
 .PHONY: install
-install: check_install
+install: check
        @set -e; for subdir in $(SUBDIRS-y); do \
                $(MAKE) -C $$subdir $@; \
        done
@@ -58,10 +58,6 @@ distclean: clean
 check:
        $(MAKE) -C check
 
-.PHONY: check_install
-check_install: check
-       $(MAKE) -C check install
-
 .PHONY: check_clean
 check_clean:
        $(MAKE) -C check clean